T:Type, eq, leq:(TT).
IsEqFun(T;eq)  Linorder(T;a,b.(a leq b))  (mk_oset(T;eq;leq)  LOSet) 

latex

Up	sets 1
Definitions of Statement	PosetSig, |p|, =, , DSet, a  b, QOSet, POSet{i}, LOSet, mk_oset(T;eq;leq)
Definitions	x,y. t(x;y), , mk_oset(T;eq;leq), t  T, x f y, P  Q, x:A. B(x), , t.2, t.1, =, DSet, QOSet, a  b, |p|, POSet{i}, LOSet, PosetSig, P & Q, Preorder(T;x,y.R(x;y)), x(s1,s2), Order(T;x,y.R(x;y)), Linorder(T;x,y.R(x;y))
Lemmas	bool wf, eqfun p wf, assert wf, linorder wf, connex wf, anti sym wf, set leq wf, preorder wf, set eq wf, set car wf